'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, p(s(0())) -> 0()
, f(X) -> n__f(X)
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ f^#(0()) -> c_0(0^#())
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, p^#(s(0())) -> c_2(0^#())
, f^#(X) -> c_3()
, s^#(X) -> c_4()
, 0^#() -> c_5()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate^#(n__0()) -> c_8(0^#())
, activate^#(X) -> c_9()}
The usable rules are:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
The estimated dependency graph contains the following edges:
{f^#(0()) -> c_0(0^#())}
==> {0^#() -> c_5()}
{f^#(s(0())) -> c_1(f^#(p(s(0()))))}
==> {f^#(X) -> c_3()}
{f^#(s(0())) -> c_1(f^#(p(s(0()))))}
==> {f^#(s(0())) -> c_1(f^#(p(s(0()))))}
{f^#(s(0())) -> c_1(f^#(p(s(0()))))}
==> {f^#(0()) -> c_0(0^#())}
{p^#(s(0())) -> c_2(0^#())}
==> {0^#() -> c_5()}
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
==> {f^#(X) -> c_3()}
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
==> {f^#(s(0())) -> c_1(f^#(p(s(0()))))}
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
==> {f^#(0()) -> c_0(0^#())}
{activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
==> {s^#(X) -> c_4()}
{activate^#(n__0()) -> c_8(0^#())}
==> {0^#() -> c_5()}
We consider the following path(s):
1) { activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, f^#(0()) -> c_0(0^#())
, 0^#() -> c_5()}
The usable rules for this path are the following:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(0()) -> c_0(0^#())
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [4]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [6]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(0()) -> c_0(0^#())}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(0()) -> c_0(0^#())}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [4]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [5]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [3]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0^#() -> c_5()}
and weakly orienting the rules
{ f^#(0()) -> c_0(0^#())
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0^#() -> c_5()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
0^#() = [1]
c_1(x1) = [1] x1 + [3]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [8]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [12]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [4]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [8]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ s(X) -> n__s(X)
, activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ 0() -> n__0()
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(X) -> n__s(X)
, activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [1]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [14]
n__f(x1) = [1] x1 + [2]
n__s(x1) = [1] x1 + [1]
n__0() = [0]
s(x1) = [1] x1 + [2]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [8]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [12]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ s(X) -> n__s(X)
, activate(n__f(X)) -> f(activate(X))
, 0() -> n__0()
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ s(X) -> n__s(X)
, activate(n__f(X)) -> f(activate(X))
, 0() -> n__0()
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 20
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(20, 21) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(22) -> 21
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(23) -> 22
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 20
, n__0_3() -> 23
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, f^#_1(14) -> 17
, f^#_2(15) -> 18
, c_0_0(1) -> 3
, c_0_1(19) -> 6
, c_0_1(19) -> 17
, c_0_2(24) -> 18
, 0^#_0() -> 1
, 0^#_1() -> 19
, 0^#_2() -> 24
, c_1_1(17) -> 3
, c_1_2(18) -> 6
, c_5_0() -> 1
, c_5_1() -> 19
, c_5_2() -> 24
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
2) { activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())
, 0^#() -> c_5()}
The usable rules for this path are the following:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()
, f^#(0()) -> c_0(0^#())
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__0()) -> 0()
, activate(X) -> X}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p(s(0())) -> 0()}
and weakly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p(s(0())) -> 0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(0()) -> c_0(0^#())}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(0()) -> c_0(0^#())}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [3]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0^#() -> c_5()}
and weakly orienting the rules
{ f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0^#() -> c_5()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [8]
c_0(x1) = [1] x1 + [1]
0^#() = [4]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [3]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [4]
c_0(x1) = [1] x1 + [1]
0^#() = [1]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [7]
c_6(x1) = [1] x1 + [3]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, 0^#() -> c_5()
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 18
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(18, 19) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(20) -> 19
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(21) -> 20
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 18
, n__0_3() -> 21
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, c_0_0(1) -> 3
, c_0_1(17) -> 6
, 0^#_0() -> 1
, 0^#_1() -> 17
, c_5_0() -> 1
, c_5_1() -> 17
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
3) { activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, f^#(0()) -> c_0(0^#())}
The usable rules for this path are the following:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(0()) -> c_0(0^#())}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(0()) -> c_0(0^#())}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [4]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [4]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [2]
0^#() = [2]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [4]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [12]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [2]
0^#() = [2]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [8]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))}
and weakly orienting the rules
{ 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [12]
n__s(x1) = [1] x1 + [5]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(X) -> n__s(X)
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(X) -> n__s(X)
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(9) -> 4
, f_1(13) -> 13
, f_2(19) -> 13
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 9
, 0_1() -> 13
, 0_2() -> 14
, 0_2() -> 19
, 0_3() -> 22
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 13
, cons_1(5, 6) -> 4
, cons_2(14, 15) -> 4
, cons_2(14, 15) -> 13
, cons_3(22, 23) -> 13
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 13
, n__f_1(4) -> 4
, n__f_1(7) -> 6
, n__f_2(9) -> 4
, n__f_2(13) -> 13
, n__f_2(16) -> 15
, n__f_3(19) -> 13
, n__f_3(24) -> 23
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 13
, n__s_1(4) -> 4
, n__s_1(8) -> 7
, n__s_2(5) -> 10
, n__s_2(13) -> 13
, n__s_2(17) -> 16
, n__s_3(14) -> 20
, n__s_3(25) -> 24
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 13
, n__0_1() -> 5
, n__0_1() -> 8
, n__0_1() -> 9
, n__0_1() -> 13
, n__0_2() -> 14
, n__0_2() -> 17
, n__0_2() -> 19
, n__0_3() -> 22
, n__0_3() -> 25
, s_0(4) -> 4
, s_1(5) -> 10
, s_1(13) -> 13
, s_2(14) -> 20
, p_1(10) -> 9
, p_2(20) -> 19
, activate_0(2) -> 4
, activate_1(2) -> 13
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(9) -> 11
, f^#_1(13) -> 12
, f^#_2(19) -> 21
, c_0_0(1) -> 3
, c_0_1(18) -> 11
, c_0_1(18) -> 12
, c_0_2(26) -> 21
, 0^#_0() -> 1
, 0^#_1() -> 18
, 0^#_2() -> 26
, c_1_1(11) -> 3
, c_1_2(21) -> 12
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(12) -> 1}
4) { activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, f^#(X) -> c_3()}
The usable rules for this path are the following:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(X) -> c_3()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [3]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [8]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [6]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [7]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [5]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [1]
n__0() = [5]
s(x1) = [1] x1 + [13]
p(x1) = [1] x1 + [4]
activate(x1) = [1] x1 + [3]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [8]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 19
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(19, 20) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(21) -> 20
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(22) -> 21
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 19
, n__0_3() -> 22
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, f^#_1(14) -> 17
, f^#_2(15) -> 18
, c_1_1(17) -> 3
, c_1_2(18) -> 6
, c_3_0() -> 1
, c_3_0() -> 3
, c_3_1() -> 6
, c_3_1() -> 17
, c_3_2() -> 18
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
5) { activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())}
The usable rules for this path are the following:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(0()) -> c_0(0^#())}
Details:
We apply the weight gap principle, strictly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [2]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [3]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p(s(0())) -> 0()}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p(s(0())) -> 0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [4]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [2]
0^#() = [2]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [5]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [8]
c_0(x1) = [1] x1 + [9]
0^#() = [1]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [12]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [3]
activate(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [7]
c_6(x1) = [1] x1 + [3]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(0()) -> c_0(0^#())}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(15) -> 4
, f_2(16) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 15
, 0_2() -> 11
, 0_2() -> 16
, 0_3() -> 18
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 8) -> 4
, cons_2(11, 12) -> 5
, cons_2(16, 12) -> 4
, cons_3(18, 19) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(9) -> 8
, n__f_2(5) -> 5
, n__f_2(13) -> 12
, n__f_2(15) -> 4
, n__f_3(16) -> 5
, n__f_3(20) -> 19
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(10) -> 9
, n__s_2(11) -> 17
, n__s_2(14) -> 13
, n__s_3(21) -> 20
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 10
, n__0_1() -> 15
, n__0_2() -> 11
, n__0_2() -> 14
, n__0_2() -> 16
, n__0_3() -> 18
, n__0_3() -> 21
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(11) -> 17
, p_1(5) -> 15
, p_2(17) -> 16
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, c_0_0(1) -> 3
, c_0_1(7) -> 6
, 0^#_0() -> 1
, 0^#_1() -> 7
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
6) { activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
The usable rules for this path are the following:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(s(0())) -> 0()
, s(X) -> n__s(X)
, 0() -> n__0()
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [2]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [4]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [8]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__s(X)) -> s(activate(X))}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__s(X)) -> s(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [8]
n__0() = [2]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [15]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [1]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [12]
c_6(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ 0() -> n__0()
, f(X) -> n__f(X)}
and weakly orienting the rules
{ activate(n__s(X)) -> s(activate(X))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ 0() -> n__0()
, f(X) -> n__f(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [10]
0() = [14]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [15]
n__0() = [13]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [15]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [15]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f(0()) -> cons(0(), n__f(n__s(n__0())))}
and weakly orienting the rules
{ 0() -> n__0()
, f(X) -> n__f(X)
, activate(n__s(X)) -> s(activate(X))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f(0()) -> cons(0(), n__f(n__s(n__0())))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [4]
0() = [6]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [1]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
activate(x1) = [1] x1 + [9]
f^#(x1) = [1] x1 + [2]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [1] x1 + [9]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [11]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(X) -> n__s(X)
, activate(n__f(X)) -> f(activate(X))
, f(s(0())) -> f(p(s(0())))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ f(0()) -> cons(0(), n__f(n__s(n__0())))
, 0() -> n__0()
, f(X) -> n__f(X)
, activate(n__s(X)) -> s(activate(X))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(X) -> n__s(X)
, activate(n__f(X)) -> f(activate(X))
, f(s(0())) -> f(p(s(0())))
, f^#(s(0())) -> c_1(f^#(p(s(0()))))}
Weak Rules:
{ f(0()) -> cons(0(), n__f(n__s(n__0())))
, 0() -> n__0()
, f(X) -> n__f(X)
, activate(n__s(X)) -> s(activate(X))
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_1(5) -> 4
, f_1(5) -> 5
, f_2(7) -> 4
, f_2(7) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 11
, 0_2() -> 7
, 0_2() -> 9
, 0_3() -> 16
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_2(9, 13) -> 4
, cons_2(9, 13) -> 5
, cons_3(16, 17) -> 4
, cons_3(16, 17) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(5) -> 4
, n__f_1(5) -> 5
, n__f_2(7) -> 4
, n__f_2(7) -> 5
, n__f_2(14) -> 13
, n__f_3(18) -> 17
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(4) -> 4
, n__s_2(5) -> 5
, n__s_2(15) -> 14
, n__s_3(9) -> 8
, n__s_3(19) -> 18
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 11
, n__0_2() -> 7
, n__0_2() -> 9
, n__0_2() -> 15
, n__0_3() -> 16
, n__0_3() -> 19
, s_0(4) -> 4
, s_1(5) -> 5
, s_2(9) -> 8
, p_1(5) -> 11
, p_2(8) -> 7
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, f^#_1(11) -> 10
, f^#_2(7) -> 12
, c_1_1(10) -> 3
, c_1_2(12) -> 6
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
7) { activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, s^#(X) -> c_4()}
The usable rules for this path are the following:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, s^#(X) -> c_4()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [7]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p(s(0())) -> 0()}
and weakly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p(s(0())) -> 0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [5]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [1]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [8]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [8]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [12]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, s^#(X) -> c_4()}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 17
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(17, 18) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(19) -> 18
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(20) -> 19
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 17
, n__0_3() -> 20
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, s^#_0(2) -> 1
, s^#_0(4) -> 3
, s^#_1(5) -> 6
, c_4_0() -> 1
, c_4_0() -> 3
, c_4_1() -> 6
, activate^#_0(2) -> 1
, c_7_0(3) -> 1
, c_7_1(6) -> 1}
8) {activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
The usable rules for this path are the following:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__0()) -> 0()
, activate(X) -> X}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
and weakly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__s(X)) -> c_7(s^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [2]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p(s(0())) -> 0()}
and weakly orienting the rules
{ activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p(s(0())) -> 0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [12]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [11]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [10]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [11]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [5]
activate(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [4]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [1] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__s(X)) -> c_7(s^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 17
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(17, 18) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(19) -> 18
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(20) -> 19
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 17
, n__0_3() -> 20
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, s^#_0(2) -> 1
, s^#_0(4) -> 3
, s^#_1(5) -> 6
, activate^#_0(2) -> 1
, c_7_0(3) -> 1
, c_7_1(6) -> 1}
9) {activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
The usable rules for this path are the following:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__0()) -> 0()
, activate(X) -> X}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [2]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p(s(0())) -> 0()}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p(s(0())) -> 0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [12]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [11]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [10]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [11]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [5]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [4]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [8]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, activate(n__0()) -> 0()
, activate(X) -> X}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 17
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(17, 18) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(19) -> 18
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(20) -> 19
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 17
, n__0_3() -> 20
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
10)
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(X) -> c_3()}
The usable rules for this path are the following:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0()
, activate(X) -> X
, s(X) -> n__s(X)
, 0() -> n__0()
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)
, p(s(0())) -> 0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, f^#(X) -> c_3()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [7]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p(s(0())) -> 0()}
and weakly orienting the rules
{ activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p(s(0())) -> 0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
and weakly orienting the rules
{ p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__f(X)) -> c_6(f^#(activate(X)))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [9]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0() -> n__0()}
and weakly orienting the rules
{ activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0() -> n__0()}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [7]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s(X) -> n__s(X)}
and weakly orienting the rules
{ 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s(X) -> n__s(X)}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [1]
n__f(x1) = [1] x1 + [0]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [5]
activate(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [8]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{activate(n__f(X)) -> f(activate(X))}
and weakly orienting the rules
{ s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate(n__f(X)) -> f(activate(X))}
Details:
Interpretation Functions:
f(x1) = [1] x1 + [0]
0() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
n__f(x1) = [1] x1 + [1]
n__s(x1) = [1] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
activate(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [15]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ activate(n__s(X)) -> s(activate(X))
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, f(X) -> n__f(X)}
Weak Rules:
{ activate(n__f(X)) -> f(activate(X))
, s(X) -> n__s(X)
, 0() -> n__0()
, activate^#(n__f(X)) -> c_6(f^#(activate(X)))
, p(s(0())) -> 0()
, activate(n__0()) -> 0()
, activate(X) -> X
, f^#(X) -> c_3()}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ f_0(4) -> 4
, f_1(5) -> 5
, f_1(14) -> 4
, f_2(15) -> 5
, 0_0() -> 4
, 0_1() -> 5
, 0_1() -> 14
, 0_2() -> 10
, 0_2() -> 15
, 0_3() -> 17
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(5, 7) -> 4
, cons_2(10, 11) -> 5
, cons_2(15, 11) -> 4
, cons_3(17, 18) -> 5
, n__f_0(2) -> 2
, n__f_0(2) -> 4
, n__f_0(2) -> 5
, n__f_1(4) -> 4
, n__f_1(8) -> 7
, n__f_2(5) -> 5
, n__f_2(12) -> 11
, n__f_2(14) -> 4
, n__f_3(15) -> 5
, n__f_3(19) -> 18
, n__s_0(2) -> 2
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_1(5) -> 4
, n__s_1(5) -> 5
, n__s_1(9) -> 8
, n__s_2(10) -> 16
, n__s_2(13) -> 12
, n__s_3(20) -> 19
, n__0_0() -> 2
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_1() -> 5
, n__0_1() -> 9
, n__0_1() -> 14
, n__0_2() -> 10
, n__0_2() -> 13
, n__0_2() -> 15
, n__0_3() -> 17
, n__0_3() -> 20
, s_1(5) -> 4
, s_1(5) -> 5
, s_2(10) -> 16
, p_1(5) -> 14
, p_2(16) -> 15
, activate_0(2) -> 4
, activate_1(2) -> 5
, f^#_0(2) -> 1
, f^#_0(4) -> 3
, f^#_1(5) -> 6
, c_3_0() -> 1
, c_3_0() -> 3
, c_3_1() -> 6
, activate^#_0(2) -> 1
, c_6_0(3) -> 1
, c_6_1(6) -> 1}
11)
{ p^#(s(0())) -> c_2(0^#())
, 0^#() -> c_5()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {0^#() -> c_5()}
Weak Rules: {p^#(s(0())) -> c_2(0^#())}
Details:
We apply the weight gap principle, strictly orienting the rules
{0^#() -> c_5()}
and weakly orienting the rules
{p^#(s(0())) -> c_2(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0^#() -> c_5()}
Details:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [1]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ 0^#() -> c_5()
, p^#(s(0())) -> c_2(0^#())}
Details:
The given problem does not contain any strict rules
12)
{p^#(s(0())) -> c_2(0^#())}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {p^#(s(0())) -> c_2(0^#())}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{p^#(s(0())) -> c_2(0^#())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(0())) -> c_2(0^#())}
Details:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [1] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {p^#(s(0())) -> c_2(0^#())}
Details:
The given problem does not contain any strict rules
13)
{activate^#(n__0()) -> c_8(0^#())}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {activate^#(n__0()) -> c_8(0^#())}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{activate^#(n__0()) -> c_8(0^#())}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(n__0()) -> c_8(0^#())}
Details:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {activate^#(n__0()) -> c_8(0^#())}
Details:
The given problem does not contain any strict rules
14)
{ activate^#(n__0()) -> c_8(0^#())
, 0^#() -> c_5()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {0^#() -> c_5()}
Weak Rules: {activate^#(n__0()) -> c_8(0^#())}
Details:
We apply the weight gap principle, strictly orienting the rules
{0^#() -> c_5()}
and weakly orienting the rules
{activate^#(n__0()) -> c_8(0^#())}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0^#() -> c_5()}
Details:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [1]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ 0^#() -> c_5()
, activate^#(n__0()) -> c_8(0^#())}
Details:
The given problem does not contain any strict rules
15)
{activate^#(X) -> c_9()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {activate^#(X) -> c_9()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{activate^#(X) -> c_9()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{activate^#(X) -> c_9()}
Details:
Interpretation Functions:
f(x1) = [0] x1 + [0]
0() = [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
n__f(x1) = [0] x1 + [0]
n__s(x1) = [0] x1 + [0]
n__0() = [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
activate(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#() = [0]
c_1(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3() = [0]
s^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
activate^#(x1) = [1] x1 + [4]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {activate^#(X) -> c_9()}
Details:
The given problem does not contain any strict rules